lean 4エラーメモ

code:memo

⋊> /V/e/w/g/l/l/my-lean-proj on main ⨯ lake update

error: ./lean_packages/mathlib/lakefile.lean: package configuration has errors

⋊> /V/e/w/g/l/l/my-lean-proj on main ⨯ lake update

mathlib: no manifest entry; deleting ./lean_packages/mathlib and cloning again

error: ./lean_packages/mathlib/lakefile.lean: package configuration has errors

code:memo

stderr:

error: .\lakefile.lean:4:8: error: expected identifier

error: .\lakefile.lean:8:9: error: expected identifier

error: .\lakefile.lean:13:9: error: expected identifier

error: .\lakefile.lean: package configuration has errors

Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

下のサンプルを参考にした方が良い。

============================

code:memo

PS D:\workspace\ghworkspace\language\lean\my-lean-proj> lake update

updating lake-packages\mathlib to revision bca93b9f1fa478d202d51efe98b90d3678695209

error: .\lake-packages\mathlib\lakefile.lean:31:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'

error: .\lake-packages\mathlib\lakefile.lean:57:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'

error: .\lake-packages\mathlib\lakefile.lean: package configuration has errors

なんもわからん。

error: could not create link from 'D:\.local\share\elan\bin\elan.exe' to 'D:\.local\share\elan\bin\lake.exe'

code:memo

$ elan self update

error: could not create link from 'D:\.local\share\elan\bin\elan.exe' to 'D:\.local\share\elan\bin\lake.exe'

参考